PittsburghV1, Main, Exploration, bibRecord, 000007

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Identifieur interne : 000007 ( Main/Exploration ); précédent : 000006; suivant : 000008

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Auteurs : Julian Biendarra [Allemagne] ; Jasmin Blanchette [Allemagne] ; Aymeric Bouzy [France] ; Martin Desharnais [Allemagne] ; Mathias Fleury [Allemagne] ; Johannes Hölzl [États-Unis] ; Ond Ej Kun Ar [Allemagne] ; Andreas Lochbihler [Suisse] ; Fabian Meier [Suisse] ; Lorenz Panny [Pays-Bas] ; Andrei Popescu [Roumanie] ; Christian Sternagel [Autriche] ; René Thiemann [Autriche] ; Dmitriy Traytel [Suisse]

Source :

RBID : Hal:hal-01592196

Abstract

We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

Url:

https://hal.inria.fr/hal-01592196

DOI: 10.1007/978-3-319-66167-4_1

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 000290
to stream Hal, to step Curation: 000290
to stream Hal, to step Checkpoint: 000007
to stream Main, to step Merge: 000007
to stream Main, to step Curation: 000007

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic</title>
<author><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID">          <orgName>Max Planck Institut für Informatik</orgName>
          <orgName type="acronym">MPII</orgName>
          <desc>            <address>              <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.mpi-inf.mpg.de/</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-507228" status="VALID">          <orgName>InstantJob</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.instantjob.fr/</ref>
          </desc>
        </hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-460393" status="VALID">          <orgName>Ludwig Maximilian University [Munich]</orgName>
          <orgName type="acronym">LMU</orgName>
          <date type="start">2016-07-19</date>
          <desc>            <address>              <addrLine>Professor-Huber-Platz 2, 80539 München, Allemagne</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.jura.uni-muenchen.de/index.html</ref>
          </desc>
        </hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID">          <orgName>Max Planck Institut für Informatik</orgName>
          <orgName type="acronym">MPII</orgName>
          <desc>            <address>              <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.mpi-inf.mpg.de/</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-87723" status="VALID">          <orgName>Computer Science Department - Carnegie Mellon University</orgName>
          <desc>            <address>              <addrLine>Computer Science Department Carnegie Mellon University Pittsburgh, PA</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cs.cmu.edu/</ref>
          </desc>
          <listRelation>            <relation active="#struct-378064" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-378064" type="direct"><org type="institution" xml:id="struct-378064" status="INCOMING">          <orgName>University of Pittsburgh</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université de Pittsburgh</orgName>
</affiliation>
</author>
<author><name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID">          <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
          <orgName type="acronym">ETH Zürich</orgName>
          <desc>            <address>              <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
              <country key="CH"></country>
            </address>
            <ref type="url">https://www.ethz.ch/</ref>
          </desc>
        </hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-73149" status="VALID"><orgName>Google Switzerland</orgName>
<desc><address><country key="CH"></country>
</address>
</desc>
<listRelation><relation active="#struct-366136" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-366136" type="direct"><org type="institution" xml:id="struct-366136" status="VALID"><orgName>Research at Google</orgName>
<desc><address><country key="US"></country>
</address>
<ref type="url">https://research.google.com/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-267766" status="VALID">          <orgName>Technische Universiteit Eindhoven</orgName>
          <orgName type="acronym">TU/e</orgName>
          <desc>            <address>              <addrLine>Postbus 5135600 MB Eindhoven</addrLine>
              <country key="NL"></country>
            </address>
            <ref type="url">https://www.tue.nl/</ref>
          </desc>
        </hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
<author><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104109" status="VALID">          <orgName>"Simion Stoilow" Institute of Mathematics</orgName>
          <orgName type="acronym">IMAR</orgName>
          <desc>            <address>              <addrLine>21, Calea Grivitei Street 010702-Bucharest, Sector 1 ROMANIA</addrLine>
              <country key="RO"></country>
            </address>
            <ref type="url">http://www.imar.ro/index.php</ref>
          </desc>
          <listRelation>            <relation active="#struct-300111" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300111" type="direct"><org type="institution" xml:id="struct-300111" status="VALID">          <orgName>Romanian Academy of Sciences</orgName>
          <desc>            <address>              <country key="RO"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Roumanie</country>
</affiliation>
</author>
<author><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID">          <orgName>Department of Computer Science [Innsbruck]</orgName>
          <desc>            <address>              <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://informatik.uibk.ac.at</ref>
          </desc>
          <listRelation>            <relation active="#struct-63989" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID">          <orgName>University of Innsbruck</orgName>
          <desc>            <address>              <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://www.uibk.ac.at/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID">          <orgName>Department of Computer Science [Innsbruck]</orgName>
          <desc>            <address>              <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://informatik.uibk.ac.at</ref>
          </desc>
          <listRelation>            <relation active="#struct-63989" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID">          <orgName>University of Innsbruck</orgName>
          <desc>            <address>              <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://www.uibk.ac.at/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID">          <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
          <orgName type="acronym">ETH Zürich</orgName>
          <desc>            <address>              <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
              <country key="CH"></country>
            </address>
            <ref type="url">https://www.ethz.ch/</ref>
          </desc>
        </hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01592196</idno>
<idno type="halId">hal-01592196</idno>
<idno type="halUri">https://hal.inria.fr/hal-01592196</idno>
<idno type="url">https://hal.inria.fr/hal-01592196</idno>
<idno type="doi">10.1007/978-3-319-66167-4_1</idno>
<date when="2017-09">2017-09</date>
<idno type="wicri:Area/Hal/Corpus">000290</idno>
<idno type="wicri:Area/Hal/Curation">000290</idno>
<idno type="wicri:Area/Hal/Checkpoint">000007</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000007</idno>
<idno type="wicri:Area/Main/Merge">000007</idno>
<idno type="wicri:Area/Main/Curation">000007</idno>
<idno type="wicri:Area/Main/Exploration">000007</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic</title>
<author><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID">          <orgName>Max Planck Institut für Informatik</orgName>
          <orgName type="acronym">MPII</orgName>
          <desc>            <address>              <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.mpi-inf.mpg.de/</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-507228" status="VALID">          <orgName>InstantJob</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.instantjob.fr/</ref>
          </desc>
        </hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-460393" status="VALID">          <orgName>Ludwig Maximilian University [Munich]</orgName>
          <orgName type="acronym">LMU</orgName>
          <date type="start">2016-07-19</date>
          <desc>            <address>              <addrLine>Professor-Huber-Platz 2, 80539 München, Allemagne</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.jura.uni-muenchen.de/index.html</ref>
          </desc>
        </hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID">          <orgName>Max Planck Institut für Informatik</orgName>
          <orgName type="acronym">MPII</orgName>
          <desc>            <address>              <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
              <country key="DE"></country>
            </address>
            <ref type="url">http://www.mpi-inf.mpg.de/</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-87723" status="VALID">          <orgName>Computer Science Department - Carnegie Mellon University</orgName>
          <desc>            <address>              <addrLine>Computer Science Department Carnegie Mellon University Pittsburgh, PA</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cs.cmu.edu/</ref>
          </desc>
          <listRelation>            <relation active="#struct-378064" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-378064" type="direct"><org type="institution" xml:id="struct-378064" status="INCOMING">          <orgName>University of Pittsburgh</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université de Pittsburgh</orgName>
</affiliation>
</author>
<author><name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID">          <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
          <orgName type="acronym">ETH Zürich</orgName>
          <desc>            <address>              <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
              <country key="CH"></country>
            </address>
            <ref type="url">https://www.ethz.ch/</ref>
          </desc>
        </hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-73149" status="VALID"><orgName>Google Switzerland</orgName>
<desc><address><country key="CH"></country>
</address>
</desc>
<listRelation><relation active="#struct-366136" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-366136" type="direct"><org type="institution" xml:id="struct-366136" status="VALID"><orgName>Research at Google</orgName>
<desc><address><country key="US"></country>
</address>
<ref type="url">https://research.google.com/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-267766" status="VALID">          <orgName>Technische Universiteit Eindhoven</orgName>
          <orgName type="acronym">TU/e</orgName>
          <desc>            <address>              <addrLine>Postbus 5135600 MB Eindhoven</addrLine>
              <country key="NL"></country>
            </address>
            <ref type="url">https://www.tue.nl/</ref>
          </desc>
        </hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
<author><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104109" status="VALID">          <orgName>"Simion Stoilow" Institute of Mathematics</orgName>
          <orgName type="acronym">IMAR</orgName>
          <desc>            <address>              <addrLine>21, Calea Grivitei Street 010702-Bucharest, Sector 1 ROMANIA</addrLine>
              <country key="RO"></country>
            </address>
            <ref type="url">http://www.imar.ro/index.php</ref>
          </desc>
          <listRelation>            <relation active="#struct-300111" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300111" type="direct"><org type="institution" xml:id="struct-300111" status="VALID">          <orgName>Romanian Academy of Sciences</orgName>
          <desc>            <address>              <country key="RO"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Roumanie</country>
</affiliation>
</author>
<author><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID">          <orgName>Department of Computer Science [Innsbruck]</orgName>
          <desc>            <address>              <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://informatik.uibk.ac.at</ref>
          </desc>
          <listRelation>            <relation active="#struct-63989" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID">          <orgName>University of Innsbruck</orgName>
          <desc>            <address>              <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://www.uibk.ac.at/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID">          <orgName>Department of Computer Science [Innsbruck]</orgName>
          <desc>            <address>              <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://informatik.uibk.ac.at</ref>
          </desc>
          <listRelation>            <relation active="#struct-63989" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID">          <orgName>University of Innsbruck</orgName>
          <desc>            <address>              <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
              <country key="AT"></country>
            </address>
            <ref type="url">http://www.uibk.ac.at/</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID">          <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
          <orgName type="acronym">ETH Zürich</orgName>
          <desc>            <address>              <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
              <country key="CH"></country>
            </address>
            <ref type="url">https://www.ethz.ch/</ref>
          </desc>
        </hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/978-3-319-66167-4_1</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>Autriche</li>
<li>France</li>
<li>Pays-Bas</li>
<li>Roumanie</li>
<li>Suisse</li>
<li>États-Unis</li>
</country>
<region><li>Pennsylvanie</li>
</region>
<settlement><li>Pittsburgh</li>
</settlement>
<orgName><li>Société Max-Planck</li>
<li>Université de Pittsburgh</li>
</orgName>
</list>
<tree><country name="Allemagne"><noRegion><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
</noRegion>
<name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
</country>
<country name="France"><noRegion><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
</noRegion>
</country>
<country name="États-Unis"><region name="Pennsylvanie"><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
</region>
</country>
<country name="Suisse"><noRegion><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
</noRegion>
<name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
</country>
<country name="Pays-Bas"><noRegion><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
</noRegion>
</country>
<country name="Roumanie"><noRegion><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
</noRegion>
</country>
<country name="Autriche"><noRegion><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
</noRegion>
<name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000007 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000007 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Amérique
   |area=    PittsburghV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:hal-01592196
   |texte=   Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
}}

This area was generated with Dilib version V0.6.38.
Data generation: Fri Jun 18 17:37:45 2021. Site generation: Fri Jun 18 18:15:47 2021

	Serveur d'exploration sur Pittsburgh
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur Pittsburgh

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri